// Types Value
sig EuroValue{}
sig Date{}
sig CharSequence{}
abstract sig User
{
userName: one CharSequence,
password: one CharSequence,
}
sig Customer extends User
{
id: one Int,
name: lone CharSequence,
surname: lone CharSequence,
email : one CharSequence,
hasBuyed : set CustomTravelPackage
}
sig Employed extends User
{
id: one Int
}
sig TravelPackage
{
id: one Int,
name: one CharSequence,
location: one CharSequence,
description: lone CharSequence,
basePrice : one EuroValue,
baseTravelElements : set TravelElement
}
sig CustomTravelPackage
{
travelPackage : one TravelPackage,
totalPrice : one EuroValue,
departureDate: one Date,
arrivalDate: one Date,
travelElements : set TravelElement
}
sig TravelElement
{
id: one Int,
name: one CharSequence,
location: one CharSequence,
description: one CharSequence,
price : one EuroValue,
type : one TravelElementType
}
sig TravelElementType
{
id: one Int,
name: one CharSequence
}
// Constraints
fact positiveInt
{
(no c1: Customer, i : Int | c1.id= i and i<=0)
(no e1: Employed, i : Int | e1.id= i and i<=0)
(no t1: TravelPackage, i : Int | t1.id= i and i<=0)
(no t1: TravelElement, i : Int | t1.id= i and i<=0)
(no t1: TravelElementType, i : Int | t1.id= i and i<=0)
}
fact uniqueIds
{
(no e1,e2 : Employed, i : Int | e1!=e2 and e1.id = i and e2.id = i)
(no c1,c2 : Customer, i : Int | c1!=c2 and c1.id = i and c2.id = i)
(no t1,t2 : TravelPackage, i : Int | t1!=t2 and t1.id = i and t2.id = i)
(no t1,t2 : TravelElement, i : Int | t1!=t2 and t1.id = i and t2.id = i)
(no t1,t2 : TravelElementType, i : Int | t1!=t2 and t1.id = i and t2.id = i )
}
fact incrementalIds
{
// CustomerIds
(all c1: Customer | ((c1.id not =1) implies (some c2 : Customer | minus[c1.id,c2.id]=1)) )
(#Customer > 0 implies some c1: Customer | c1.id=1)
//EmployedIds
(all e1: Employed | ((e1.id not =1) implies (some e2 : Employed | minus[e1.id,e2.id]=1)) )
(#Employed > 0 implies some e1: Employed | e1.id=1)
// TravelPackageIds
(all t1: TravelPackage | (( t1.id not =1) implies (some t2 : TravelPackage | minus[t1.id,t2.id]=1)) )
(#TravelPackage > 0 implies some t1: TravelPackage | t1.id=1)
// TravelElementIds
(all t1: TravelElement | (( t1.id not =1) implies (some t2 : TravelElement | minus[t1.id,t2.id]=1)) )
(#TravelElement > 0 implies some t1: TravelElement | t1.id=1)
// TravelElementTypeIds
(all t1: TravelElementType | (( t1.id not =1) implies (some t2 : TravelElementType | minus[t1.id,t2.id]=1)) )
(#TravelElementType > 0 implies some t1: TravelElementType | t1.id=1)
}
fact uniqueUserName{
no u1,u2 : User, un : CharSequence | u1!=u2 and u1.userName = un and u2.userName = un
}
fact uniqueEmail{
no u1,u2 : Customer, em : CharSequence | u1!=u2 and u1.email = em and u2.email = em
}
fact distinctReturnDepartureDates
{
no t1 : CustomTravelPackage | t1.departureDate = t1.arrivalDate
}
// Predicates
pred show{
#Customer = 1
#Employed = 1
#CustomTravelPackage = 1
#TravelPackage =1
#TravelElement = 4
#TravelElementType = 2
#Date =2

}
run show